\begin{tabbing}
$\forall$${\it es}$:ES, $e$, ${\it e'}$:E.
\\[0ex]($\uparrow$isrcv($e$))
\\[0ex]$\Rightarrow$ \=($\forall$${\it e'}$:E.\+
\\[0ex]($\uparrow$isrcv(${\it e'}$)) $\Rightarrow$ (kind(${\it e'}$) = kind($e$) $\in$ Knd) $\Rightarrow$ (sender(${\it e'}$) = sender($e$) $\in$ E) $\Rightarrow$ (${\it e'}$ = $e$))
\-\\[0ex]$\Rightarrow$ ($\uparrow$isrcv(${\it e'}$))
\\[0ex]$\Rightarrow$ (kind(${\it e'}$) = kind($e$) $\in$ Knd)
\\[0ex]$\Rightarrow$ sender($e$) $\leq$loc sender(${\it e'}$) 
\\[0ex]$\Rightarrow$ $e$ $\leq$loc ${\it e'}$ 
\end{tabbing}